…ot-rules corrections, drain fix)

Review blockers from Wren (three: E1 deployment-gate assumption, compatible-
mode cross-slot legality unsupported, proof-surface overclaim) and Dawn (two:
CROSSSLOT enforced on single-shard cluster-enabled nodes falsifies the A/B-in-
compatible premise; renew=PEXPIRE makes any temporal drain gate unsound).

Spec: A2/A3 rewritten (declared-keys slot check, undeclared-KEYS prohibition,
slot rules from compatible onward as working assumption + pre-G3 probe);
migration reordered A->B->backfill->drain->C entirely in disabled mode with
compatible after C; C-gate now participation-based (B renew-migrates old-key
leases; observed-zero, never wait-a-TTL); per-phase operation table for all
six directory ops; proof scope stated honestly (write-side under E1);
Deployment Gate section discharging E1 with rollback matrix and phase gauge;
1.5.0 receipts (verified free single-node); prior-art section (Stripe,
GitLab, BullMQ, Sidekiq, Grafana, ioredis #1842) with locality contract and
executable cross-slot validator in G2; failure-modes table extended.

Model: mode variable disabled/compatible/enabled with slot rules from
compatible; MigrateB (renew-migrate, same generation); RollbackPhase +
DowngradePod with drain + reverse-max-merge guards; EnterCompatible/
RevertCompatible/EnableCluster doors; Inv_ClusterSafe -> Inv_SlotRulesSafe.
A's generation dual-write removed: mutation testing proved it redundant.
TLC green (12636 states, 3637 distinct); 9 mutants (M1-M9) all killed by
their intended invariants.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

Header still said A dual-writes the generation (removed after mutation
testing); acquire-section comment lumped O in with the both-keyspace
scripts (O touches only the old pair, itself cross-slot). Comments only;
TLC re-run green, state count unchanged.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

Review round 2 (Dawn) found the safety model could not distinguish the
B2 fix from its absence: unguarded ExpireOld lets the C-gate be
discharged by luck, so deleting MigrateB left all invariants green.
Added DrainSpec/Probe_NotC — TLC from the stall state (full-B fleet, live
old-key lease, no spontaneous expiry) with inverted verdict semantics:
violation proves C reachable (93/44); mutant M10 (MigrateB removed =
round-1 behavior) stays green, making the round-1 bug permanently
visible. Main safety model unchanged (12636/3637, M1-M9 all killed).

Also per Dawn N1: rollback matrix now names B->A as dropping every
migrated session (A renews the old key; nobody renews the migrated
lease; renewer treats Lost as fatal) — liveness cost, prefer forward-fix.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

TLC halts at the first violation, so generated/distinct counts on the
drain probe's PASS run vary with worker count and scheduling (9/8 at
-workers 1, ~100/~45 at -workers 4 — Dawn measured 114/50). Removed the
count from the run transcript and noted only the verdict is the check;
exhaustive-pass counts remain deterministic and cited.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

The drain-reachability probe (M10) guaranteed nothing mechanically: it was
a documented procedure a reviewer had to remember to run. Deleting
MigrateB leaves all five safety invariants green, so nothing in CI would
have caught the round-1 bug coming back.

scripts/check-tla-specs.sh runs both configs with opposite pass
conditions: the safety model must complete with no violation, and the
drain probe must report `Invariant Probe_NotC is violated` — a green drain
run means phase C is unreachable from the stall state and fails the build.

The inverted assertion greps the specific invariant name rather than
checking TLC's exit status: a parse error or missing module also exits
non-zero, and treating that as the expected violation would make the check
useless exactly when the spec is broken. tla2tools is pinned by release
tag and by sha256, since release assets can be re-uploaded.

Verified in four directions on the committed script: unmodified specs exit
0; MigrateB stripped from DrainNext exits 1 via the green-drain branch;
a spec that fails to parse exits 1 via the neither-verdict branch; a jar
with the wrong checksum exits 1 before TLC runs. Runtime is ~3s including
the jar download.

The module allow-list is deliberately just RedisClusterFencingMigration,
not a glob over docs/spec/*.cfg: MultiTenantRelay does not finish in a
reasonable CI budget and GitOnObjectStore explores ~12.4M states, so
attaching them to every PR would buy flakiness rather than safety.

Co-authored-by: Dawn (sprout agent) <c6237ef84fa537c78dcee78efd2d4e59f728859c7f194da42ac51ededfa0be05@sprout-oss.stage.blox.sqprod.co>
Signed-off-by: tlongwell-block <109685178+tlongwell-block@users.noreply.github.com>

Dawn's P3 replica-subtraction measurement (2026-07-30, receipts in
RESEARCH/BB_PUBLIC_REDIS_P3_ENGINE_CPU_DECOMPOSITION.md) resolves the
open <25%-decomposition caveat and lands three spec updates:

- D1 gets its gated input: ~40% of primary engine CPU is write-apply +
  publish propagation (the never-read replica carries 7.8pp of 19.5pp);
  ~60% is client-facing and divides only as connections/subscriptions
  redistribute. Notes the A4 dependency (propagation confines to the
  owning shard only after P2) plus two measurement cautions: the
  pub/sub-vs-keyed regression split is unidentifiable (r=0.997), and
  the apparent sublinearity is a ~1.1% fixed baseline.
- Fallback row corrected: the replica is not idle — 7.8% is its own
  unsheddable load on a ~3.8d doubling, saturating alone in ~14 days.
  Kickoff's 'idles at 7%' framing removed.
- Problem statement gains the measured fit window: sharp onset
  2026-07-21 ~18:00Z; fits must start post-onset; curr_connections
  moves in pool-config plateaus, not demand. Onset unattributed
  pending deploy history.

Summary timeline row updated to the fitted ~7d-to-80% with the
degraded-fallback note. Model and configs untouched; doc only.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

Dawn's delta review at 3292b35 caught the doc carrying two runways:
the problem statement still held kickoff's eyeballed ~3.5-4d doubling /
8-10d saturation, while the summary row read the fitted ~7d-to-80% —
and the eyeball figure was fitted across exactly the Jul-21-18:00Z
regime boundary the adjacent fit-window bullet forbids.

Problem statement now leads with the fitted post-onset clock (~3.4-3.5d
doubling, ~7d to 80%, r2=0.92) and demotes the kickoff figures to a
declared pre-onset eyeball. Same treatment for the ~150x/~400x family
growth (fitted: x9.6-12.4 over 9 days). G0's gate description (line
~595) keeps its original tasking text deliberately.

Model and configs untouched; doc only.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

…way band, optionality framing

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

…ml moved on main)

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

… 1.4d

Dawn's Correction 2: stacked levers multiply M, days add — 1.882 x 1.330
x 1.111 = 2.782 -> 5.09d at Td=3.45d (4.93d interaction-aware). The ~3.4d
figure required Td=2.55d, a fast-edge result reported as central. Also
reconciles the kickoff-era r8g '~1.5 days' at line 90 to the fitted 1.4d
used everywhere else. Conclusion unchanged: no infra lever outruns the
curve.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

Dawn's residual on 5baf0a1: the inline derivation used 1.33x, above
the doc's own cited ~25-30% single-thread range — a kickoff eyeball
rounded up past its ceiling and presented as derived. Restated as the
vendor range 1.25-1.30x -> 1.1-1.3d, explicitly unbenchmarked. Wall
sentence takes the optimistic edge (+1.3d) and restacks: M = 1.882 x
1.30 x 1.111 = 2.718 -> ~5.0d (interaction-aware 2.633 -> 4.8d).
Conclusion unchanged: still ~4x short of the 21d likely migration.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>

… a deploy

Dawn's onset-attribution finding (RESEARCH/BB_PUBLIC_REDIS_ONSET_ATTRIBUTION.md):
onset moves 18:00Z -> 16:40Z (15-min bins blurred it); attributed to organic
community creation (58 -> 425 in 2h, same 5-min bin as the Redis breakout,
flat subs-per-connection ratio excludes a code change). Community creation is
now linear (~3,100/day) but Redis load stays exponential — intensification
within communities — so the watch metric is channels-per-community. Adds the
four-account cacheclusterid Datadog trap (must scope aws_account:433851229429).
No planning number changes: 3.45d doubling and 5.2-9.0d band stand.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>